|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (oponent) ; Řehák, Vojtěch (oponent) ; Vojnar, Tomáš (vedoucí práce)
The subject of the thesis is to design new hardware verification techniques optimized for a process of HW/SW co-design in which hardware and software are developed in parallel to speed up the development of new embedded systems. Currently, microprocessor co-design tools typically allow to verify designs by simulation and/or functional verification. However, even extensive functional verification can miss some non-trivial bugs. Therefore, formal verification has become more and more desirable in recent years. As opposed to testing and bug-hunting techniques that only aim at detecting flaws, the goal of formal verification is to rigorously prove that the system is indeed correct. Formal verification is, however, a very demanding task, and even though a lot of progress has been achieved in this area, formal verification is far from being able to fully automatically check all relevant properties of complex designs without a significant and costly human involvement in the verification process. The thesis deals with these challenges by focusing on verification techniques based on formal approaches, but possibly relaxing or limiting their precision and generality to achieve full automation. Further, the thesis also focuses on the efficiency of the proposed techniques and their ability to deliver continuous feedback about the verification process. Special attention is devoted to the development of formal methods for checking the equivalence of microprocessor designs on various levels of abstraction. Although these designs cannot be behaviorally equivalent, they are required to give mutually corresponding results when executing the same input program, which is a property difficult to achieve. As another considered topic, the thesis proposes methods for checking correctness of mechanisms preventing data and control hazards in single-pipelined implementations of microprocessors. The approaches described in this thesis has been implemented in the form of several tools which, after examining designs of multiple pipelined microprocessors, were able to deliver promising experimental results.
|
|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (oponent) ; Řehák, Vojtěch (oponent) ; Vojnar, Tomáš (vedoucí práce)
The subject of the thesis is to design new hardware verification techniques optimized for a process of HW/SW co-design in which hardware and software are developed in parallel to speed up the development of new embedded systems. Currently, microprocessor co-design tools typically allow to verify designs by simulation and/or functional verification. However, even extensive functional verification can miss some non-trivial bugs. Therefore, formal verification has become more and more desirable in recent years. As opposed to testing and bug-hunting techniques that only aim at detecting flaws, the goal of formal verification is to rigorously prove that the system is indeed correct. Formal verification is, however, a very demanding task, and even though a lot of progress has been achieved in this area, formal verification is far from being able to fully automatically check all relevant properties of complex designs without a significant and costly human involvement in the verification process. The thesis deals with these challenges by focusing on verification techniques based on formal approaches, but possibly relaxing or limiting their precision and generality to achieve full automation. Further, the thesis also focuses on the efficiency of the proposed techniques and their ability to deliver continuous feedback about the verification process. Special attention is devoted to the development of formal methods for checking the equivalence of microprocessor designs on various levels of abstraction. Although these designs cannot be behaviorally equivalent, they are required to give mutually corresponding results when executing the same input program, which is a property difficult to achieve. As another considered topic, the thesis proposes methods for checking correctness of mechanisms preventing data and control hazards in single-pipelined implementations of microprocessors. The approaches described in this thesis has been implemented in the form of several tools which, after examining designs of multiple pipelined microprocessors, were able to deliver promising experimental results.
|
|
| |
|
|
Kombinované lineární a nelineární časově heteronomní tlumení ve vnitřní dynamice nelineárních parametrických soustav
Hortel, Milan ; Škuderová, Alena
Při projektování vysokootáčkových planetových převodových soustav o minimálních dimenzích a hmotnostech nejsou v tomto stadiu návrhu konstrukcí předem dostatečně známé mnohé funkcionální závislosti parametrů jako např. konstantní či časově heteronomní tlumení v záběrech ozubení kinematických dvojic apod. Je proto nutné, aby se základní výzkum v této oblasti, vzhledem k bezpečnosti a spolehlivosti soustav, hlouběji zabýval jak kvalitativně tak i kvantitativně analyticky i numericky touto problematikou. Hodnoty a funkcionální závislosti např. tlumících parametrů řešených systémů se mnohdy pouze odhadují a v teoretických analýzách se pak vlivy odchylek odhadovaných velikostí parametrů od jejich skutečných hodnot variačně řeší v širších předpokládaných rozsazích a tudíž i možných důsledků na vnitřní dynamiku těchto systémů. Na modelu jedné větve silového toku pseudoplanetové slabě a silně nelineární soustavy o šesti stupních volnosti jsou v této studii analyzovány bifurkační rezonanční charakteristiky relativního pohybu ozubení v záběru soustavy s kombinovaných lineárním a nelineárním - kvadratickým časově heteronomním tlumením.
|
|
| |
|
| |
|
|
K numerické analýze singularit v rezonančních charakteristikách nelineárních parametrických systémů s rázovými jevy v záběru ozubení
Hortel, Milan ; Škuderová, Alena
Rázové jevy v záběru ozubení jsou specifickým fenoménem v dynamickém výzkumu vysokorychlostních lehkých převodových systémů s kinematickými vazbami. Jsou způsobeny většími dynamickými než staticko-elastickými deformacemi zabírajících zubových profilů. V podmínkách vnitřní dynamiky jsou způsobeny mj. heteronomními tuhostními funkcemi v záběru ozubení a rezonančním naladěním tuhostní hladiny. Tlumení v záběru ozubení a v soustavě významně ovlivňuje amplitudový vývoj, velikost a fázový posuv relativního pohybu vůči tuhostní funkci resp. vůči jejímu modifikovanému tvaru v záběru ozubení. V souvislosti s tím a dalšími vlivy vystupují v rezonančních charakteristikách jistá singulární místa se skokovým amplitudovým průběhem.
|
|
| |
|
|
K vlivu tlumení na rázové jevy v záběru ozubení
Hortel, Milan ; Škuderová, Alena
Pohybové rovnice nelineární parametrické soustavy s kinematickými dvojicemi s elasticky uloženými ozubenými koly byly sestaveny na základě analytické Lagrangeovy teorie, principu virtuální práce, d´Alembertova principu převedení problému kinetiky na statiku a Lagrangeova principu uvolnění a analyticky řešeny soustavou ekvivalentních nelineárních integrodiferenciálních rovnic s řešícími jádry ve tvaru rozštěpených Greenových rezolvent. Vliv lineárního a nelineárního tlumení v jednotlivých fázích zubového záběru na rázové jevy v záběru ozubení je v tomto příspěvku řešen numerickou simulací v prostředí MATLAB/Simulink.
|
|
| |
host ::
RSS.